ПРИМЕНЕНИЕ ИНКРЕМЕНТАЛЬНЫХ SAT-РЕШАТЕЛЕЙ ДЛЯ РЕШЕНИЯ NP-ТРУДНЫХ ЗАДАЧ НА ПРИМЕРЕ ЗАДАЧИ СИНТЕЗА МИНИМАЛЬНЫХ БУЛЕВЫХ ФОРМУЛ
Аннотация:
Предмет исследования. Рассмотрен метод решения NP-трудной задачи синтеза минимальной булевой формулы по заданной таблице истинности. Предложено решение указанной задачи, основанное на ее сведении к задаче выполнимости булевой формулы (SAT). Рассмотрены вопросы эффективной и удобной программной реализации сведений NP-трудных задач к SAT. Метод. Для решения задачи синтеза минимальной булевой формулы используется подход программирования в ограничениях: для заданной таблицы истинности строится SAT-формула, выполнимая тогда и только тогда, когда существует искомая булева формула заданного размера, удовлетворяющая заданной таблице. Отличительной особенностью разработанного метода является возможность использования инкрементальных программных средств для решения SAT (SAT-решателей). Основные результаты. Предложен метод синтеза минимальной по числу операторов и терминалов булевой формулы по заданной таблице истинности. Метод основан на сведении к SAT и позволяет использовать инкрементальные SAT-решатели. Разработан фреймворк kotlin-satlib, позволяющий эффективно и удобно использовать языки Kotlin и Java для программной реализации сведения различных NP-трудных задач к SAT, пользуясь нативным взаимодействием с SAT-решателями посредством технологии JNI. Предложенный метод синтеза минимальной булевой формулы реализован на языке программирования Kotlin с использованием разработанного фреймворка kotlin-satlib. Практическая значимость. Экспериментальное исследование на примере синтеза минимальной булевой формулы показало, что использование инкрементальных SAT-решателей для решения NP-трудных задач является целесообразным, поскольку позволяет уменьшить суммарное время решения задач по сравнению с использованием неинкрементального подхода.
Ключевые слова:
Постоянный URL
Статьи в номере
- ИСПОЛЬЗОВАНИЕ НАВЕДЕННЫХ МЕХАНИЧЕСКИХ НАПРЯЖЕНИЙ ПРИ ФОРМООБРАЗОВАНИИ СФЕРИЧЕСКИХ ПОВЕРХНОСТЕЙ ПОДЛОЖЕК ИНТЕРФЕРЕНЦИОННЫХ ЗЕРКАЛ
- ИССЛЕДОВАНИЕ ИЗМЕНЕНИЯ ЧУВСТВИТЕЛЬНОСТИ НАКЛОННОЙ ВОЛОКОННОЙ БРЭГГОВСКОЙ РЕШЕТКИ ПРИ ЕЕ ХИМИЧЕСКОМ ТРАВЛЕНИИ
- ОСОБЕННОСТИ ПРИМЕНЕНИЯ ОПТИЧЕСКИХ ПОЛИМЕРОВ ПРИ ПРОЕКТИРОВАНИИ ОПТИЧЕСКИХ СИСТЕМ
- ОЦЕНКА ВЛИЯНИЯ РАСТИТЕЛЬНЫХ ЭКСТРАКТОВ НА АКТИВНОСТЬ ЗОЛОТИСТОГО СТАФИЛОКОККА МЕТОДОМ ЭЛЕКТРОХИМИЧЕСКОГО БИОТЕСТИРОВАНИЯ
- БЫСТРЫЙ АЛГОРИТМ ОЦЕНКИ ДВИЖЕНИЯ В ВИДЕОКОДЕКЕ СТАНДАРТА HEVC
- МОДИФИКАЦИЯ МЕТОДА СОВМЕСТНОЙ КЛАСТЕРИЗАЦИИ В ГРАФОВОМ И КОРРЕЛЯЦИОННОМ ПРОСТРАНСТВАХ
- ПРИМЕНЕНИЕ КОНЦЕПЦИИ ЦИФРОВЫХ ДВОЙНИКОВ НА ЭТАПАХ ЖИЗНЕННОГО ЦИКЛА ПРОИЗВОДСТВЕННЫХ СИСТЕМ
- ОПТИМИЗАЦИЯ ГИПЕРПАРАМЕТРОВ НА ОСНОВЕ ОБЪЕДИНЕНИЯ АПРИОРНЫХ И АПОСТЕРИОРНЫХ ЗНАНИЙ О ЗАДАЧЕ КЛАССИФИКАЦИИ
- ВЫВОД ГЕННЫХ РЕГУЛЯТОРНЫХ СЕТЕЙ ПО ДАННЫМ ЭКСПРЕССИИ ГЕНОВ ПРИ ПОМОЩИ БАЙЕСОВСКИХ СЕТЕЙ
- ОЦЕНИВАНИЕ РАСПРЕДЕЛЕНИЯ ОТРАЖАТЕЛЬНЫХ ХАРАКТЕРИСТИК ПРИ КВАЗИНЕПРЕРЫВНОМ СВЕРХШИРОКОПОЛОСНОМ ЗОНДИРУЮЩЕМ СИГНАЛЕ
- АДАПТИВНАЯ ЗАДАЧА О РАСШИРЕННОМ ВОСПРОИЗВОДСТВЕ ПРИ МИНИМИЗАЦИИ ОБОБЩЕННЫХ ЗАТРАТ
- ПРЕДСКАЗАНИЕ УСЛОВИЙ РЕАКЦИЙ С ПОМОЩЬЮ МЕТОДОВ ГЛУБОКОГО ОБУЧЕНИЯ
- МОДЕЛИРОВАНИЕ ВЕРТИКАЛЬНЫХ СВЕТИЛЬНИКОВ ДЛЯ ДНЕВНОГО ОСВЕЩЕНИЯ ВНУТРЕННИХ ПОМЕЩЕНИЙ ПРОМЫШЛЕННЫХ ЗДАНИЙ(на англ. яз.)
- УРАВНЕНИЕ СОСТОЯНИЯ ПОЛИМЕРНЫХ НИТЕЙ
- ПРОГНОЗИРОВАНИЕ МЕХАНИЧЕСКИХ СВОЙСТВ ОДНОМЕРНЫХ ПОЛИМЕРНЫХ СТРУКТУР
- ПРИМЕНЕНИЕ МЕТОДА НЕЗАВИСИМЫХ КОМПОНЕНТ ДЛЯ ОПРЕДЕЛЕНИЯ НАЧАЛЬНОГО ПРИБЛИЖЕНИЯ ПРИ ПОИСКЕ АКТИВНЫХ МОДУЛЕЙ В БИОЛОГИЧЕСКИХ ГРАФАХ
- СИСТЕМА ПОДДЕРЖКИ КЛИНИЧЕСКИХ РЕШЕНИЙ С ОБРАБОТКОЙ МУЛЬТИМОДАЛЬНЫХ МЕДИЦИНСКИХ ДАННЫХ КАК СРЕДСТВО ПОВЫШЕНИЯ ЭФФЕКТИВНОСТИ РАБОТЫ ВРАЧА-РАДИОЛОГА